:: LATSUBGR semantic presentation

K135() is Element of K19(K131())

K131() is set

K19(K131()) is non empty set

K130() is set

K19(K130()) is non empty set

K19(K135()) is non empty set

K134() is set

{} is set

the Function-like functional empty set is Function-like functional empty set

1 is non empty set

G1 is non empty Group-like V130() L11()

G2 is non empty Group-like Subgroup of G1

f is non empty Group-like Subgroup of G1

G2 /\ f is non empty strict Group-like Subgroup of G1

the carrier of (G2 /\ f) is non empty set

the carrier of G2 is non empty set

the carrier of f is non empty set

the carrier of G2 /\ the carrier of f is set

carr f is Element of K19( the carrier of G1)

the carrier of G1 is non empty set

K19( the carrier of G1) is non empty set

carr G2 is Element of K19( the carrier of G1)

(carr G2) /\ (carr f) is Element of K19( the carrier of G1)

G1 is non empty Group-like V130() L11()

Subgroups G1 is non empty set

G2 is set

f is non empty strict Group-like Subgroup of G1

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

K19( the carrier of G1) is non empty set

G2 is Element of K19( the carrier of G1)

gr G2 is non empty strict Group-like Subgroup of G1

f is non empty strict Group-like Subgroup of G1

the carrier of f is non empty set

carr f is Element of K19( the carrier of G1)

gr (carr f) is non empty strict Group-like Subgroup of G1

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

K19( the carrier of G1) is non empty set

G2 is non empty Group-like Subgroup of G1

the carrier of G2 is non empty set

f is non empty Group-like Subgroup of G1

the carrier of f is non empty set

the carrier of G2 \/ the carrier of f is set

G2 "\/" f is non empty strict Group-like Subgroup of G1

carr G2 is Element of K19( the carrier of G1)

carr f is Element of K19( the carrier of G1)

(carr G2) \/ (carr f) is Element of K19( the carrier of G1)

gr ((carr G2) \/ (carr f)) is non empty strict Group-like Subgroup of G1

a is Element of K19( the carrier of G1)

gr a is non empty strict Group-like Subgroup of G1

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like Subgroup of G1

f is non empty Group-like Subgroup of G1

G2 "\/" f is non empty strict Group-like Subgroup of G1

carr G2 is Element of K19( the carrier of G1)

K19( the carrier of G1) is non empty set

carr f is Element of K19( the carrier of G1)

(carr G2) \/ (carr f) is Element of K19( the carrier of G1)

gr ((carr G2) \/ (carr f)) is non empty strict Group-like Subgroup of G1

a is Element of the carrier of G1

the carrier of G2 is non empty set

the carrier of f is non empty set

the carrier of G2 \/ the carrier of f is set

b is Element of K19( the carrier of G1)

gr b is non empty strict Group-like Subgroup of G1

the carrier of G2 is non empty set

the carrier of f is non empty set

the carrier of G2 \/ the carrier of f is set

b is Element of K19( the carrier of G1)

gr b is non empty strict Group-like Subgroup of G1

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) V137(G1,G2) Element of K19(K20( the carrier of G1, the carrier of G2))

a is non empty Group-like Subgroup of G1

the carrier of a is non empty set

f .: the carrier of a is Element of K19( the carrier of G2)

K19( the carrier of G2) is non empty set

1_ G1 is Element of the carrier of G1

f . (1_ G1) is Element of the carrier of G2

A1 is Element of the carrier of G2

A1 " is Element of the carrier of G2

B1 is Element of the carrier of G1

f . B1 is Element of the carrier of G2

B1 " is Element of the carrier of G1

f . (B1 ") is Element of the carrier of G2

(f . B1) " is Element of the carrier of G2

A1 is Element of the carrier of G2

B1 is Element of the carrier of G2

A1 * B1 is Element of the carrier of G2

A is Element of the carrier of G1

f . A is Element of the carrier of G2

B is Element of the carrier of G1

f . B is Element of the carrier of G2

A * B is Element of the carrier of G1

f . (A * B) is Element of the carrier of G2

(f . A) * (f . B) is Element of the carrier of G2

dom f is Element of K19( the carrier of G1)

K19( the carrier of G1) is non empty set

b is Element of the carrier of G2

A1 is non empty strict Group-like Subgroup of G2

the carrier of A1 is non empty set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) V137(G1,G2) Element of K19(K20( the carrier of G1, the carrier of G2))

a is non empty Group-like Subgroup of G2

the carrier of a is non empty set

f " the carrier of a is Element of K19( the carrier of G1)

K19( the carrier of G1) is non empty set

b is Element of the carrier of G1

b " is Element of the carrier of G1

f . b is Element of the carrier of G2

(f . b) " is Element of the carrier of G2

f . (b ") is Element of the carrier of G2

b is Element of the carrier of G1

A1 is Element of the carrier of G1

b * A1 is Element of the carrier of G1

f . A1 is Element of the carrier of G2

f . b is Element of the carrier of G2

(f . b) * (f . A1) is Element of the carrier of G2

f . (b * A1) is Element of the carrier of G2

1_ G2 is Element of the carrier of G2

1_ G1 is Element of the carrier of G1

f . (1_ G1) is Element of the carrier of G2

b is non empty strict Group-like Subgroup of G1

the carrier of b is non empty set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) V137(G1,G2) Element of K19(K20( the carrier of G1, the carrier of G2))

a is non empty Group-like Subgroup of G1

the carrier of a is non empty set

f .: the carrier of a is Element of K19( the carrier of G2)

K19( the carrier of G2) is non empty set

b is non empty Group-like Subgroup of G1

the carrier of b is non empty set

f .: the carrier of b is Element of K19( the carrier of G2)

A1 is non empty Group-like Subgroup of G2

the carrier of A1 is non empty set

B1 is non empty Group-like Subgroup of G2

the carrier of B1 is non empty set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) V137(G1,G2) Element of K19(K20( the carrier of G1, the carrier of G2))

a is non empty Group-like Subgroup of G2

the carrier of a is non empty set

f " the carrier of a is Element of K19( the carrier of G1)

K19( the carrier of G1) is non empty set

b is non empty Group-like Subgroup of G2

the carrier of b is non empty set

f " the carrier of b is Element of K19( the carrier of G1)

A1 is non empty Group-like Subgroup of G1

the carrier of A1 is non empty set

B1 is non empty Group-like Subgroup of G1

the carrier of B1 is non empty set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

K19( the carrier of G1) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) Element of K19(K20( the carrier of G1, the carrier of G2))

a is Element of K19( the carrier of G1)

f .: a is Element of K19( the carrier of G2)

K19( the carrier of G2) is non empty set

gr a is non empty strict Group-like Subgroup of G1

the carrier of (gr a) is non empty set

f .: the carrier of (gr a) is Element of K19( the carrier of G2)

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

K19( the carrier of G1) is non empty set

A1 is Element of K19( the carrier of G1)

f is non empty Group-like Subgroup of G1

the carrier of f is non empty set

a is non empty Group-like Subgroup of G1

the carrier of a is non empty set

the carrier of f \/ the carrier of a is set

b is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) Element of K19(K20( the carrier of G1, the carrier of G2))

f "\/" a is non empty strict Group-like Subgroup of G1

carr f is Element of K19( the carrier of G1)

carr a is Element of K19( the carrier of G1)

(carr f) \/ (carr a) is Element of K19( the carrier of G1)

gr ((carr f) \/ (carr a)) is non empty strict Group-like Subgroup of G1

the carrier of (f "\/" a) is non empty set

b .: the carrier of (f "\/" a) is Element of K19( the carrier of G2)

K19( the carrier of G2) is non empty set

gr A1 is non empty strict Group-like Subgroup of G1

the carrier of (gr A1) is non empty set

b .: the carrier of (gr A1) is Element of K19( the carrier of G2)

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

K19( the carrier of G1) is non empty set

1_ G1 is Element of the carrier of G1

{(1_ G1)} is set

(1). G1 is non empty strict Group-like Subgroup of G1

G2 is Element of K19( the carrier of G1)

gr G2 is non empty strict Group-like Subgroup of G1

the carrier of ((1). G1) is non empty set

G1 is non empty Group-like V130() L11()

Subgroups G1 is non empty set

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is set

f is non empty strict Group-like Subgroup of G1

carr f is Element of K19( the carrier of G1)

a is Element of K19( the carrier of G1)

b is non empty strict Group-like Subgroup of G1

the carrier of b is non empty set

G2 is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

f is non empty strict Group-like Subgroup of G1

G2 . f is set

the carrier of f is non empty set

G2 is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

f is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

a is set

G2 . a is set

f . a is set

b is non empty strict Group-like Subgroup of G1

the carrier of b is non empty set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

Subgroups G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is non empty strict Group-like Subgroup of G1

(G1) . G2 is set

f is Element of the carrier of G1

the carrier of G2 is non empty set

the carrier of G2 is non empty set

G1 is non empty Group-like V130() L11()

1_ G1 is Element of the carrier of G1

the carrier of G1 is non empty set

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

Subgroups G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is non empty strict Group-like Subgroup of G1

(G1) . G2 is set

the carrier of G2 is non empty set

1_ G2 is Element of the carrier of G2

G1 is non empty Group-like V130() L11()

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

Subgroups G1 is non empty set

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is non empty strict Group-like Subgroup of G1

(G1) . G2 is set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

Subgroups G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is non empty strict Group-like Subgroup of G1

(G1) . G2 is set

f is Element of the carrier of G1

a is Element of the carrier of G1

f * a is Element of the carrier of G1

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

Subgroups G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is non empty strict Group-like Subgroup of G1

(G1) . G2 is set

f is Element of the carrier of G1

f " is Element of the carrier of G1

G1 is non empty Group-like V130() L11()

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

Subgroups G1 is non empty set

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is non empty strict Group-like Subgroup of G1

f is non empty strict Group-like Subgroup of G1

G2 /\ f is non empty strict Group-like Subgroup of G1

the carrier of (G2 /\ f) is non empty set

(G1) . G2 is set

(G1) . f is set

((G1) . G2) /\ ((G1) . f) is set

the carrier of G2 is non empty set

the carrier of f is non empty set

G1 is non empty Group-like V130() L11()

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

Subgroups G1 is non empty set

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is non empty strict Group-like Subgroup of G1

f is non empty strict Group-like Subgroup of G1

G2 /\ f is non empty strict Group-like Subgroup of G1

(G1) . (G2 /\ f) is set

(G1) . G2 is set

(G1) . f is set

((G1) . G2) /\ ((G1) . f) is set

the carrier of (G2 /\ f) is non empty set

G1 is non empty Group-like V130() L11()

Subgroups G1 is non empty set

K19((Subgroups G1)) is non empty set

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

G2 is non empty Element of K19((Subgroups G1))

(G1) .: G2 is Element of K19((bool the carrier of G1))

K19((bool the carrier of G1)) is non empty set

meet ((G1) .: G2) is Element of K19( the carrier of G1)

a is Element of Subgroups G1

(G1) . a is Element of bool the carrier of G1

f is Element of K19(K19( the carrier of G1))

meet f is Element of K19( the carrier of G1)

a is Element of the carrier of G1

a " is Element of the carrier of G1

A1 is set

B1 is Element of K19( the carrier of G1)

A is Element of Subgroups G1

(G1) . A is Element of bool the carrier of G1

B is non empty strict Group-like Subgroup of G1

the carrier of B is non empty set

b is Element of the carrier of G1

b " is Element of the carrier of G1

a is Element of the carrier of G1

b is Element of the carrier of G1

a * b is Element of the carrier of G1

A is set

B is Element of K19( the carrier of G1)

B3 is Element of Subgroups G1

(G1) . B3 is Element of bool the carrier of G1

C1 is non empty strict Group-like Subgroup of G1

the carrier of C1 is non empty set

B1 is Element of the carrier of G1

A1 is Element of the carrier of G1

A1 * B1 is Element of the carrier of G1

1_ G1 is Element of the carrier of G1

a is set

b is Element of K19( the carrier of G1)

A1 is Element of Subgroups G1

(G1) . A1 is Element of bool the carrier of G1

B1 is non empty strict Group-like Subgroup of G1

the carrier of B1 is non empty set

f is non empty strict Group-like Subgroup of G1

the carrier of f is non empty set

a is non empty strict Group-like Subgroup of G1

the carrier of a is non empty set

G1 is non empty Group-like V130() L11()

Subgroups G1 is non empty set

K19((Subgroups G1)) is non empty set

(1). G1 is non empty strict Group-like Subgroup of G1

G2 is non empty Element of K19((Subgroups G1))

(G1,G2) is non empty strict Group-like Subgroup of G1

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

f is Element of Subgroups G1

(G1) . f is Element of bool the carrier of G1

the carrier of ((1). G1) is non empty set

(G1) .: G2 is Element of K19((bool the carrier of G1))

K19((bool the carrier of G1)) is non empty set

1_ G1 is Element of the carrier of G1

{(1_ G1)} is set

meet ((G1) .: G2) is Element of K19( the carrier of G1)

the carrier of (G1,G2) is non empty set

G1 is non empty Group-like V130() L11()

Subgroups G1 is non empty set

K19((Subgroups G1)) is non empty set

G2 is Element of Subgroups G1

{G2} is set

f is non empty Element of K19((Subgroups G1))

(G1,f) is non empty strict Group-like Subgroup of G1

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

dom (G1) is Element of K19((Subgroups G1))

Im ((G1),G2) is set

(G1) .: {G2} is set

meet (Im ((G1),G2)) is set

(G1) . G2 is Element of bool the carrier of G1

{((G1) . G2)} is set

meet {((G1) . G2)} is set

the carrier of (G1,f) is non empty set

(G1) .: f is Element of K19((bool the carrier of G1))

K19((bool the carrier of G1)) is non empty set

meet ((G1) .: f) is Element of K19( the carrier of G1)

a is non empty strict Group-like Subgroup of G1

the carrier of a is non empty set

G1 is non empty Group-like V130() L11()

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

G2 is non empty Group-like Subgroup of G1

f is non empty Group-like Subgroup of G1

G2 "\/" f is non empty strict Group-like Subgroup of G1

the carrier of G1 is non empty set

carr G2 is Element of K19( the carrier of G1)

K19( the carrier of G1) is non empty set

carr f is Element of K19( the carrier of G1)

(carr G2) \/ (carr f) is Element of K19( the carrier of G1)

gr ((carr G2) \/ (carr f)) is non empty strict Group-like Subgroup of G1

a is Element of the carrier of (lattice G1)

b is Element of the carrier of (lattice G1)

a "\/" b is Element of the carrier of (lattice G1)

(SubJoin G1) . (a,b) is set

G1 is non empty Group-like V130() L11()

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

G2 is non empty Group-like Subgroup of G1

f is non empty Group-like Subgroup of G1

G2 /\ f is non empty strict Group-like Subgroup of G1

a is Element of the carrier of (lattice G1)

b is Element of the carrier of (lattice G1)

a "/\" b is Element of the carrier of (lattice G1)

(SubMeet G1) . (a,b) is set

G1 is non empty Group-like V130() L11()

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

G2 is Element of the carrier of (lattice G1)

f is non empty Group-like Subgroup of G1

G1 is non empty Group-like V130() L11()

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

G2 is non empty Group-like Subgroup of G1

f is non empty Group-like Subgroup of G1

the carrier of G2 is non empty set

the carrier of f is non empty set

a is Element of the carrier of (lattice G1)

b is Element of the carrier of (lattice G1)

a "/\" b is Element of the carrier of (lattice G1)

the L_meet of (lattice G1) is Relation-like K20( the carrier of (lattice G1), the carrier of (lattice G1)) -defined the carrier of (lattice G1) -valued Function-like non empty V14(K20( the carrier of (lattice G1), the carrier of (lattice G1))) V18(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)) Element of K19(K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)))

K20( the carrier of (lattice G1), the carrier of (lattice G1)) is non empty set

K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)) is non empty set

K19(K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1))) is non empty set

the L_meet of (lattice G1) . (a,b) is Element of the carrier of (lattice G1)

G2 /\ f is non empty strict Group-like Subgroup of G1

the carrier of G2 /\ the carrier of f is set

G2 /\ f is non empty strict Group-like Subgroup of G1

the L_meet of (lattice G1) is Relation-like K20( the carrier of (lattice G1), the carrier of (lattice G1)) -defined the carrier of (lattice G1) -valued Function-like non empty V14(K20( the carrier of (lattice G1), the carrier of (lattice G1))) V18(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)) Element of K19(K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)))

K20( the carrier of (lattice G1), the carrier of (lattice G1)) is non empty set

K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)) is non empty set

K19(K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1))) is non empty set

the L_meet of (lattice G1) . (a,b) is Element of the carrier of (lattice G1)

a "/\" b is Element of the carrier of (lattice G1)

G1 is non empty Group-like V130() L11()

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

G2 is non empty Group-like Subgroup of G1

f is non empty Group-like Subgroup of G1

a is Element of the carrier of (lattice G1)

b is Element of the carrier of (lattice G1)

the carrier of G2 is non empty set

the carrier of f is non empty set

G2 /\ f is non empty strict Group-like Subgroup of G1

the L_meet of (lattice G1) is Relation-like K20( the carrier of (lattice G1), the carrier of (lattice G1)) -defined the carrier of (lattice G1) -valued Function-like non empty V14(K20( the carrier of (lattice G1), the carrier of (lattice G1))) V18(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)) Element of K19(K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)))

K20( the carrier of (lattice G1), the carrier of (lattice G1)) is non empty set

K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1)) is non empty set

K19(K20(K20( the carrier of (lattice G1), the carrier of (lattice G1)), the carrier of (lattice G1))) is non empty set

the L_meet of (lattice G1) . (a,b) is Element of the carrier of (lattice G1)

a "/\" b is Element of the carrier of (lattice G1)

G1 is non empty Group-like V130() L11()

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

K19( the carrier of (lattice G1)) is non empty set

G2 is Element of K19( the carrier of (lattice G1))

Top (lattice G1) is Element of the carrier of (lattice G1)

f is Element of the carrier of (lattice G1)

f is Element of the carrier of (lattice G1)

K19((Subgroups G1)) is non empty set

f is non empty Element of K19((Subgroups G1))

(G1,f) is non empty strict Group-like Subgroup of G1

a is Element of the carrier of (lattice G1)

the Element of f is Element of f

A1 is Element of the carrier of (lattice G1)

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

A is Element of Subgroups G1

(G1) . A is Element of bool the carrier of G1

B1 is non empty strict Group-like Subgroup of G1

the carrier of B1 is non empty set

(G1) .: f is Element of K19((bool the carrier of G1))

K19((bool the carrier of G1)) is non empty set

meet ((G1) .: f) is Element of K19( the carrier of G1)

the carrier of (G1,f) is non empty set

A1 is Element of the carrier of (lattice G1)

the carrier of G1 is non empty set

bool the carrier of G1 is non empty Element of K19(K19( the carrier of G1))

K19( the carrier of G1) is non empty set

K19(K19( the carrier of G1)) is non empty set

(G1) is Relation-like Subgroups G1 -defined bool the carrier of G1 -valued Function-like non empty V14( Subgroups G1) V18( Subgroups G1, bool the carrier of G1) Element of K19(K20((Subgroups G1),(bool the carrier of G1)))

K20((Subgroups G1),(bool the carrier of G1)) is non empty set

K19(K20((Subgroups G1),(bool the carrier of G1))) is non empty set

(G1) .: f is Element of K19((bool the carrier of G1))

K19((bool the carrier of G1)) is non empty set

B1 is non empty Group-like Subgroup of G1

the carrier of B1 is non empty set

A is set

B is Element of K19( the carrier of G1)

B3 is Element of Subgroups G1

(G1) . B3 is Element of bool the carrier of G1

C1 is Element of the carrier of (lattice G1)

C3 is non empty strict Group-like Subgroup of G1

the carrier of C3 is non empty set

(G1) . the Element of f is Element of bool the carrier of G1

meet ((G1) .: f) is Element of K19( the carrier of G1)

the carrier of (G1,f) is non empty set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

lattice G2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G2 is non empty set

SubJoin G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

K20((Subgroups G2),(Subgroups G2)) is non empty set

K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)) is non empty set

K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2))) is non empty set

SubMeet G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

LattStr(# (Subgroups G2),(SubJoin G2),(SubMeet G2) #) is non empty strict LattStr

the carrier of (lattice G2) is non empty set

K20( the carrier of (lattice G1), the carrier of (lattice G2)) is non empty set

K19(K20( the carrier of (lattice G1), the carrier of (lattice G2))) is non empty set

K19( the carrier of G2) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) Element of K19(K20( the carrier of G1, the carrier of G2))

a is set

b is non empty strict Group-like Subgroup of G1

the carrier of b is non empty set

f .: the carrier of b is Element of K19( the carrier of G2)

gr (f .: the carrier of b) is non empty strict Group-like Subgroup of G2

A1 is non empty strict Group-like Subgroup of G2

B1 is Element of the carrier of (lattice G2)

A is non empty strict Group-like Subgroup of G1

B is Element of K19( the carrier of G2)

the carrier of A is non empty set

f .: the carrier of A is Element of K19( the carrier of G2)

gr (f .: the carrier of A) is non empty strict Group-like Subgroup of G2

a is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G2) -valued Function-like non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G2)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G2)))

b is non empty strict Group-like Subgroup of G1

the carrier of b is non empty set

f .: the carrier of b is Element of K19( the carrier of G2)

a . b is set

A1 is Element of K19( the carrier of G2)

gr A1 is non empty strict Group-like Subgroup of G2

a is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G2) -valued Function-like non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G2)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G2)))

b is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G2) -valued Function-like non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G2)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G2)))

A1 is set

a . A1 is set

b . A1 is set

B1 is non empty strict Group-like Subgroup of G1

the carrier of B1 is non empty set

f .: the carrier of B1 is Element of K19( the carrier of G2)

gr (f .: the carrier of B1) is non empty strict Group-like Subgroup of G2

G1 is non empty Group-like V130() L11()

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

the carrier of G1 is non empty set

id the carrier of G1 is Relation-like the carrier of G1 -defined the carrier of G1 -valued Function-like one-to-one non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G1) Element of K19(K20( the carrier of G1, the carrier of G1))

K20( the carrier of G1, the carrier of G1) is non empty set

K19(K20( the carrier of G1, the carrier of G1)) is non empty set

(G1,G1,(id the carrier of G1)) is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G1) -valued Function-like non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G1)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G1)))

K20( the carrier of (lattice G1), the carrier of (lattice G1)) is non empty set

K19(K20( the carrier of (lattice G1), the carrier of (lattice G1))) is non empty set

id the carrier of (lattice G1) is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G1) -valued Function-like one-to-one non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G1)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G1)))

f is set

(G1,G1,(id the carrier of G1)) . f is set

a is non empty strict Group-like Subgroup of G1

the carrier of a is non empty set

(id the carrier of G1) .: the carrier of a is Element of K19( the carrier of G1)

K19( the carrier of G1) is non empty set

b is set

A1 is Element of the carrier of G1

(id the carrier of G1) . A1 is Element of the carrier of G1

b is set

A1 is Element of the carrier of G1

B1 is Element of the carrier of G1

(id the carrier of G1) . B1 is Element of the carrier of G1

(G1,G1,(id the carrier of G1)) . a is set

b is Element of K19( the carrier of G1)

gr b is non empty strict Group-like Subgroup of G1

dom (G1,G1,(id the carrier of G1)) is Element of K19( the carrier of (lattice G1))

K19( the carrier of (lattice G1)) is non empty set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) V137(G1,G2) Element of K19(K20( the carrier of G1, the carrier of G2))

(G1,G2,f) is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G2) -valued Function-like non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G2)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G2)))

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

lattice G2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G2 is non empty set

SubJoin G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

K20((Subgroups G2),(Subgroups G2)) is non empty set

K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)) is non empty set

K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2))) is non empty set

SubMeet G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

LattStr(# (Subgroups G2),(SubJoin G2),(SubMeet G2) #) is non empty strict LattStr

the carrier of (lattice G2) is non empty set

K20( the carrier of (lattice G1), the carrier of (lattice G2)) is non empty set

K19(K20( the carrier of (lattice G1), the carrier of (lattice G2))) is non empty set

dom (G1,G2,f) is Element of K19( the carrier of (lattice G1))

K19( the carrier of (lattice G1)) is non empty set

1_ G1 is Element of the carrier of G1

f . (1_ G1) is Element of the carrier of G2

b is set

A1 is set

(G1,G2,f) . b is set

(G1,G2,f) . A1 is set

K19( the carrier of G2) is non empty set

B1 is non empty strict Group-like Subgroup of G1

the carrier of B1 is non empty set

f .: the carrier of B1 is Element of K19( the carrier of G2)

A is non empty strict Group-like Subgroup of G1

the carrier of A is non empty set

f .: the carrier of A is Element of K19( the carrier of G2)

C1 is Element of the carrier of G2

C1 " is Element of the carrier of G2

C3 is Element of the carrier of G1

f . C3 is Element of the carrier of G2

C3 " is Element of the carrier of G1

f . (C3 ") is Element of the carrier of G2

(f . C3) " is Element of the carrier of G2

C1 is Element of the carrier of G2

C3 is Element of the carrier of G2

C1 * C3 is Element of the carrier of G2

A3 is Element of the carrier of G1

f . A3 is Element of the carrier of G2

AA is Element of the carrier of G1

f . AA is Element of the carrier of G2

A3 * AA is Element of the carrier of G1

f . (A3 * AA) is Element of the carrier of G2

(f . A3) * (f . AA) is Element of the carrier of G2

C1 is Element of the carrier of G2

C1 " is Element of the carrier of G2

C3 is Element of the carrier of G1

f . C3 is Element of the carrier of G2

C3 " is Element of the carrier of G1

f . (C3 ") is Element of the carrier of G2

(f . C3) " is Element of the carrier of G2

dom f is Element of K19( the carrier of G1)

K19( the carrier of G1) is non empty set

C1 is Element of the carrier of G2

C3 is Element of the carrier of G2

C1 * C3 is Element of the carrier of G2

A3 is Element of the carrier of G1

f . A3 is Element of the carrier of G2

AA is Element of the carrier of G1

f . AA is Element of the carrier of G2

A3 * AA is Element of the carrier of G1

f . (A3 * AA) is Element of the carrier of G2

(f . A3) * (f . AA) is Element of the carrier of G2

(G1,G2,f) . B1 is set

B is Element of K19( the carrier of G2)

gr B is non empty strict Group-like Subgroup of G2

(G1,G2,f) . A is set

B3 is Element of K19( the carrier of G2)

gr B3 is non empty strict Group-like Subgroup of G2

C1 is Element of the carrier of G2

C1 is non empty strict Group-like Subgroup of G2

the carrier of C1 is non empty set

a is Element of the carrier of G2

gr (f .: the carrier of A) is non empty strict Group-like Subgroup of G2

C3 is non empty strict Group-like Subgroup of G2

the carrier of C3 is non empty set

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

(1). G1 is non empty strict Group-like Subgroup of G1

(1). G2 is non empty strict Group-like Subgroup of G2

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) V137(G1,G2) Element of K19(K20( the carrier of G1, the carrier of G2))

(G1,G2,f) is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G2) -valued Function-like non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G2)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G2)))

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

lattice G2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G2 is non empty set

SubJoin G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

K20((Subgroups G2),(Subgroups G2)) is non empty set

K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)) is non empty set

K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2))) is non empty set

SubMeet G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

LattStr(# (Subgroups G2),(SubJoin G2),(SubMeet G2) #) is non empty strict LattStr

the carrier of (lattice G2) is non empty set

K20( the carrier of (lattice G1), the carrier of (lattice G2)) is non empty set

K19(K20( the carrier of (lattice G1), the carrier of (lattice G2))) is non empty set

(G1,G2,f) . ((1). G1) is set

K19( the carrier of G2) is non empty set

the carrier of ((1). G1) is non empty set

f .: the carrier of ((1). G1) is Element of K19( the carrier of G2)

a is Element of K19( the carrier of G2)

1_ G1 is Element of the carrier of G1

{(1_ G1)} is set

f .: {(1_ G1)} is Element of K19( the carrier of G2)

1_ G2 is Element of the carrier of G2

f . (1_ G1) is Element of the carrier of G2

b is set

A1 is Element of the carrier of G2

B1 is Element of the carrier of G1

f . B1 is Element of the carrier of G2

{(1_ G2)} is set

gr a is non empty strict Group-like Subgroup of G2

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

lattice G2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G2 is non empty set

SubJoin G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

K20((Subgroups G2),(Subgroups G2)) is non empty set

K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)) is non empty set

K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2))) is non empty set

SubMeet G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

LattStr(# (Subgroups G2),(SubJoin G2),(SubMeet G2) #) is non empty strict LattStr

the carrier of (lattice G2) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) V137(G1,G2) Element of K19(K20( the carrier of G1, the carrier of G2))

(G1,G2,f) is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G2) -valued Function-like non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G2)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G2)))

K20( the carrier of (lattice G1), the carrier of (lattice G2)) is non empty set

K19(K20( the carrier of (lattice G1), the carrier of (lattice G2))) is non empty set

a is Element of the carrier of (lattice G1)

b is Element of the carrier of (lattice G1)

a "/\" b is Element of the carrier of (lattice G1)

(G1,G2,f) . (a "/\" b) is Element of the carrier of (lattice G2)

(G1,G2,f) . a is Element of the carrier of (lattice G2)

(G1,G2,f) . b is Element of the carrier of (lattice G2)

((G1,G2,f) . a) "/\" ((G1,G2,f) . b) is Element of the carrier of (lattice G2)

A1 is non empty strict Group-like Subgroup of G1

B1 is non empty strict Group-like Subgroup of G1

the carrier of B1 is non empty set

f .: the carrier of B1 is Element of K19( the carrier of G2)

K19( the carrier of G2) is non empty set

A is Element of the carrier of G2

B is Element of the carrier of G2

A * B is Element of the carrier of G2

B3 is Element of the carrier of G1

f . B3 is Element of the carrier of G2

C1 is Element of the carrier of G1

f . C1 is Element of the carrier of G2

B3 * C1 is Element of the carrier of G1

f . (B3 * C1) is Element of the carrier of G2

(f . B3) * (f . C1) is Element of the carrier of G2

A is Element of the carrier of G2

A " is Element of the carrier of G2

B is Element of the carrier of G1

f . B is Element of the carrier of G2

B " is Element of the carrier of G1

f . (B ") is Element of the carrier of G2

(f . B) " is Element of the carrier of G2

the carrier of A1 is non empty set

f .: the carrier of A1 is Element of K19( the carrier of G2)

A is Element of the carrier of G2

A " is Element of the carrier of G2

B is Element of the carrier of G1

f . B is Element of the carrier of G2

B " is Element of the carrier of G1

f . (B ") is Element of the carrier of G2

(f . B) " is Element of the carrier of G2

1_ G1 is Element of the carrier of G1

A1 /\ B1 is non empty strict Group-like Subgroup of G1

(G1,G2,f) . (A1 /\ B1) is set

the carrier of (A1 /\ B1) is non empty set

f .: the carrier of (A1 /\ B1) is Element of K19( the carrier of G2)

gr (f .: the carrier of (A1 /\ B1)) is non empty strict Group-like Subgroup of G2

A is non empty strict Group-like Subgroup of G1

B is Element of the carrier of G2

B3 is Element of the carrier of G2

B * B3 is Element of the carrier of G2

C1 is Element of the carrier of G1

f . C1 is Element of the carrier of G2

C3 is Element of the carrier of G1

f . C3 is Element of the carrier of G2

C1 * C3 is Element of the carrier of G1

f . (C1 * C3) is Element of the carrier of G2

(f . C1) * (f . C3) is Element of the carrier of G2

gr (f .: the carrier of A1) is non empty strict Group-like Subgroup of G2

gr (f .: the carrier of B1) is non empty strict Group-like Subgroup of G2

dom f is Element of K19( the carrier of G1)

K19( the carrier of G1) is non empty set

the carrier of A is non empty set

f .: the carrier of A is Element of K19( the carrier of G2)

B is Element of the carrier of G2

B3 is Element of the carrier of G2

B * B3 is Element of the carrier of G2

C1 is Element of the carrier of G1

f . C1 is Element of the carrier of G2

C3 is Element of the carrier of G1

f . C3 is Element of the carrier of G2

C1 * C3 is Element of the carrier of G1

f . (C1 * C3) is Element of the carrier of G2

(f . C1) * (f . C3) is Element of the carrier of G2

B is Element of the carrier of G2

B " is Element of the carrier of G2

B3 is Element of the carrier of G1

f . B3 is Element of the carrier of G2

B3 " is Element of the carrier of G1

f . (B3 ") is Element of the carrier of G2

(f . B3) " is Element of the carrier of G2

f . (1_ G1) is Element of the carrier of G2

B is Element of the carrier of G2

B is non empty strict Group-like Subgroup of G2

the carrier of B is non empty set

B3 is Element of the carrier of G2

B3 is non empty strict Group-like Subgroup of G2

the carrier of B3 is non empty set

C1 is Element of the carrier of G2

C1 is non empty strict Group-like Subgroup of G2

the carrier of C1 is non empty set

C1 /\ B3 is non empty strict Group-like Subgroup of G2

the carrier of (C1 /\ B3) is non empty set

C3 is set

A3 is Element of the carrier of G2

AA is Element of the carrier of G1

f . AA is Element of the carrier of G2

the carrier of A1 /\ the carrier of B1 is set

C3 is set

A3 is Element of the carrier of G2

AA is Element of the carrier of G1

f . AA is Element of the carrier of G2

the carrier of A1 /\ the carrier of B1 is set

C3 is set

A3 is Element of the carrier of G2

AA is Element of the carrier of G1

f . AA is Element of the carrier of G2

the carrier of C1 /\ the carrier of B3 is set

C3 is set

the carrier of C1 /\ the carrier of B3 is set

the carrier of A1 /\ the carrier of B1 is set

f .: ( the carrier of A1 /\ the carrier of B1) is Element of K19( the carrier of G2)

(gr (f .: the carrier of A1)) /\ (gr (f .: the carrier of B1)) is non empty strict Group-like Subgroup of G2

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

lattice G2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G2 is non empty set

SubJoin G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

K20((Subgroups G2),(Subgroups G2)) is non empty set

K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)) is non empty set

K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2))) is non empty set

SubMeet G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

LattStr(# (Subgroups G2),(SubJoin G2),(SubMeet G2) #) is non empty strict LattStr

the carrier of (lattice G2) is non empty set

f is Relation-like the carrier of G1 -defined the carrier of G2 -valued Function-like non empty V14( the carrier of G1) V18( the carrier of G1, the carrier of G2) V137(G1,G2) Element of K19(K20( the carrier of G1, the carrier of G2))

(G1,G2,f) is Relation-like the carrier of (lattice G1) -defined the carrier of (lattice G2) -valued Function-like non empty V14( the carrier of (lattice G1)) V18( the carrier of (lattice G1), the carrier of (lattice G2)) Element of K19(K20( the carrier of (lattice G1), the carrier of (lattice G2)))

K20( the carrier of (lattice G1), the carrier of (lattice G2)) is non empty set

K19(K20( the carrier of (lattice G1), the carrier of (lattice G2))) is non empty set

a is Element of the carrier of (lattice G1)

b is Element of the carrier of (lattice G1)

a "\/" b is Element of the carrier of (lattice G1)

(G1,G2,f) . (a "\/" b) is Element of the carrier of (lattice G2)

(G1,G2,f) . a is Element of the carrier of (lattice G2)

(G1,G2,f) . b is Element of the carrier of (lattice G2)

((G1,G2,f) . a) "\/" ((G1,G2,f) . b) is Element of the carrier of (lattice G2)

A1 is non empty strict Group-like Subgroup of G1

B1 is non empty strict Group-like Subgroup of G1

the carrier of B1 is non empty set

f .: the carrier of B1 is Element of K19( the carrier of G2)

K19( the carrier of G2) is non empty set

A is Element of the carrier of G2

A " is Element of the carrier of G2

B is Element of the carrier of G1

f . B is Element of the carrier of G2

B " is Element of the carrier of G1

f . (B ") is Element of the carrier of G2

(f . B) " is Element of the carrier of G2

1_ G1 is Element of the carrier of G1

the carrier of A1 is non empty set

f . (1_ G1) is Element of the carrier of G2

K19( the carrier of G1) is non empty set

the carrier of A1 \/ the carrier of B1 is set

f .: the carrier of A1 is Element of K19( the carrier of G2)

B is Element of the carrier of G2

B " is Element of the carrier of G2

B3 is Element of the carrier of G1

f . B3 is Element of the carrier of G2

B3 " is Element of the carrier of G1

f . (B3 ") is Element of the carrier of G2

(f . B3) " is Element of the carrier of G2

(f .: the carrier of A1) \/ (f .: the carrier of B1) is Element of K19( the carrier of G2)

dom f is Element of K19( the carrier of G1)

B3 is Element of the carrier of G2

C1 is Element of the carrier of G2

B3 * C1 is Element of the carrier of G2

C3 is Element of the carrier of G1

f . C3 is Element of the carrier of G2

A3 is Element of the carrier of G1

f . A3 is Element of the carrier of G2

C3 * A3 is Element of the carrier of G1

f . (C3 * A3) is Element of the carrier of G2

(f . C3) * (f . A3) is Element of the carrier of G2

A1 "\/" B1 is non empty strict Group-like Subgroup of G1

carr A1 is Element of K19( the carrier of G1)

carr B1 is Element of K19( the carrier of G1)

(carr A1) \/ (carr B1) is Element of K19( the carrier of G1)

gr ((carr A1) \/ (carr B1)) is non empty strict Group-like Subgroup of G1

(G1,G2,f) . (A1 "\/" B1) is set

the carrier of (A1 "\/" B1) is non empty set

f .: the carrier of (A1 "\/" B1) is Element of K19( the carrier of G2)

gr (f .: the carrier of (A1 "\/" B1)) is non empty strict Group-like Subgroup of G2

B3 is Element of the carrier of G2

B3 is non empty strict Group-like Subgroup of G2

the carrier of B3 is non empty set

C1 is Element of the carrier of G2

C3 is Element of the carrier of G2

C1 * C3 is Element of the carrier of G2

A3 is Element of the carrier of G1

f . A3 is Element of the carrier of G2

AA is Element of the carrier of G1

f . AA is Element of the carrier of G2

A3 * AA is Element of the carrier of G1

f . (A3 * AA) is Element of the carrier of G2

(f . A3) * (f . AA) is Element of the carrier of G2

gr (f .: the carrier of A1) is non empty strict Group-like Subgroup of G2

gr (f .: the carrier of B1) is non empty strict Group-like Subgroup of G2

C1 is non empty strict Group-like Subgroup of G1

the carrier of C1 is non empty set

f .: the carrier of C1 is Element of K19( the carrier of G2)

C3 is Element of the carrier of G2

A3 is Element of the carrier of G2

C3 * A3 is Element of the carrier of G2

AA is Element of the carrier of G1

f . AA is Element of the carrier of G2

H is Element of the carrier of G1

f . H is Element of the carrier of G2

AA * H is Element of the carrier of G1

f . (AA * H) is Element of the carrier of G2

(f . AA) * (f . H) is Element of the carrier of G2

C3 is Element of the carrier of G2

C3 " is Element of the carrier of G2

A3 is Element of the carrier of G1

f . A3 is Element of the carrier of G2

A3 " is Element of the carrier of G1

f . (A3 ") is Element of the carrier of G2

(f . A3) " is Element of the carrier of G2

C3 is Element of the carrier of G2

C3 is non empty strict Group-like Subgroup of G2

the carrier of C3 is non empty set

A3 is Element of the carrier of G2

A3 is non empty strict Group-like Subgroup of G2

the carrier of A3 is non empty set

A3 "\/" B3 is non empty strict Group-like Subgroup of G2

carr A3 is Element of K19( the carrier of G2)

carr B3 is Element of K19( the carrier of G2)

(carr A3) \/ (carr B3) is Element of K19( the carrier of G2)

gr ((carr A3) \/ (carr B3)) is non empty strict Group-like Subgroup of G2

the carrier of (A3 "\/" B3) is non empty set

AA is set

H is Element of the carrier of G2

x is Element of the carrier of G1

f . x is Element of the carrier of G2

A is Element of K19( the carrier of G1)

gr A is non empty strict Group-like Subgroup of G1

the carrier of (gr A) is non empty set

AA is set

H is Element of the carrier of G2

x is Element of the carrier of G1

f . x is Element of the carrier of G2

A is Element of K19( the carrier of G1)

gr A is non empty strict Group-like Subgroup of G1

the carrier of (gr A) is non empty set

B is Element of K19( the carrier of G2)

gr B is non empty strict Group-like Subgroup of G2

the carrier of (gr B) is non empty set

f " the carrier of A3 is Element of K19( the carrier of G1)

f " the carrier of B3 is Element of K19( the carrier of G1)

(f " the carrier of A3) \/ (f " the carrier of B3) is Element of K19( the carrier of G1)

f " the carrier of (A3 "\/" B3) is Element of K19( the carrier of G1)

H is Element of the carrier of G1

H " is Element of the carrier of G1

f . H is Element of the carrier of G2

(f . H) " is Element of the carrier of G2

f . (H ") is Element of the carrier of G2

A is Element of K19( the carrier of G1)

AA is Element of K19( the carrier of G1)

H is Element of the carrier of G1

x is Element of the carrier of G1

H * x is Element of the carrier of G1

f . x is Element of the carrier of G2

f . H is Element of the carrier of G2

(f . H) * (f . x) is Element of the carrier of G2

f . (H * x) is Element of the carrier of G2

H is set

f . H is set

1_ G2 is Element of the carrier of G2

H is non empty strict Group-like Subgroup of G1

the carrier of H is non empty set

x is set

f . x is set

gr A is non empty strict Group-like Subgroup of G1

the carrier of (gr A) is non empty set

f .: (f " the carrier of (A3 "\/" B3)) is Element of K19( the carrier of G2)

x is set

x is Element of the carrier of G2

c

f . c

(gr (f .: the carrier of A1)) "\/" (gr (f .: the carrier of B1)) is non empty strict Group-like Subgroup of G2

carr (gr (f .: the carrier of A1)) is Element of K19( the carrier of G2)

carr (gr (f .: the carrier of B1)) is Element of K19( the carrier of G2)

(carr (gr (f .: the carrier of A1))) \/ (carr (gr (f .: the carrier of B1))) is Element of K19( the carrier of G2)

gr ((carr (gr (f .: the carrier of A1))) \/ (carr (gr (f .: the carrier of B1)))) is non empty strict Group-like Subgroup of G2

G1 is non empty Group-like V130() L11()

the carrier of G1 is non empty set

G2 is non empty Group-like V130() L11()

the carrier of G2 is non empty set

K20( the carrier of G1, the carrier of G2) is non empty set

K19(K20( the carrier of G1, the carrier of G2)) is non empty set

lattice G1 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G1 is non empty set

SubJoin G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

K20((Subgroups G1),(Subgroups G1)) is non empty set

K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)) is non empty set

K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1))) is non empty set

SubMeet G1 is Relation-like K20((Subgroups G1),(Subgroups G1)) -defined Subgroups G1 -valued Function-like non empty V14(K20((Subgroups G1),(Subgroups G1))) V18(K20((Subgroups G1),(Subgroups G1)), Subgroups G1) Element of K19(K20(K20((Subgroups G1),(Subgroups G1)),(Subgroups G1)))

LattStr(# (Subgroups G1),(SubJoin G1),(SubMeet G1) #) is non empty strict LattStr

the carrier of (lattice G1) is non empty set

lattice G2 is non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() LattStr

Subgroups G2 is non empty set

SubJoin G2 is Relation-like K20((Subgroups G2),(Subgroups G2)) -defined Subgroups G2 -valued Function-like non empty V14(K20((Subgroups G2),(Subgroups G2))) V18(K20((Subgroups G2),(Subgroups G2)), Subgroups G2) Element of K19(K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)))

K20((Subgroups G2),(Subgroups G2)) is non empty set

K20(K20((Subgroups G2),(Subgroups G2)),(Subgroups G2)) is non empty set

K19(K20(K20((Subgroups G2),(Subgroups G2)),(