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
c18 is Element of the carrier of G1
f . c18 is Element of 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
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)),(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