:: LATSUBGR semantic presentation

begin

theorem :: LATSUBGR:1
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds the carrier of (H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) /\ H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) = the carrier of H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) /\ the carrier of H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) ;

theorem :: LATSUBGR:2
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for h being ( ( ) ( ) set ) holds
( h : ( ( ) ( ) set ) in Subgroups G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) iff ex H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st h : ( ( ) ( ) set ) = H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ;

theorem :: LATSUBGR:3
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for A being ( ( ) ( ) Subset of )
for H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st A : ( ( ) ( ) Subset of ) = the carrier of H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) holds
gr A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) = H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

theorem :: LATSUBGR:4
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = the carrier of H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) \/ the carrier of H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) holds
H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) "\/" H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) = gr A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

theorem :: LATSUBGR:5
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st ( g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) or g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) holds
g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) "\/" H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

theorem :: LATSUBGR:6
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for H1 being ( ( ) ( non empty Group-like ) Subgroup of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ex H2 being ( ( strict ) ( non empty strict Group-like ) Subgroup of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st the carrier of H2 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) = f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) .: the carrier of H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUBGR:7
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for H2 being ( ( ) ( non empty Group-like ) Subgroup of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ex H1 being ( ( strict ) ( non empty strict Group-like ) Subgroup of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st the carrier of H1 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) = f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) " the carrier of H2 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUBGR:8
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for H3, H4 being ( ( ) ( non empty Group-like ) Subgroup of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st the carrier of H3 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) = f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) .: the carrier of H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & the carrier of H4 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) = f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) .: the carrier of H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is ( ( ) ( non empty Group-like ) Subgroup of H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) holds
H3 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is ( ( ) ( non empty Group-like ) Subgroup of H4 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ;

theorem :: LATSUBGR:9
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for H3, H4 being ( ( ) ( non empty Group-like ) Subgroup of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st the carrier of H3 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) = f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) " the carrier of H1 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & the carrier of H4 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) = f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) " the carrier of H2 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) & H1 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is ( ( ) ( non empty Group-like ) Subgroup of H2 : ( ( ) ( non empty Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) holds
H3 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is ( ( ) ( non empty Group-like ) Subgroup of H4 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ;

theorem :: LATSUBGR:10
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) holds f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) .: A : ( ( ) ( ) Subset of ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) c= f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) .: the carrier of (gr A : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUBGR:11
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = the carrier of H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) \/ the carrier of H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) set ) holds
f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) .: the carrier of (H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) "\/" H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) = f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) .: the carrier of (gr A : ( ( ) ( ) Subset of ) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUBGR:12
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = {(1_ G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) set ) holds
gr A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) = (1). G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

definition
let G be ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ;
func carr G -> ( ( Function-like V18( Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) , bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) -defined bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) V18( Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) , bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) , bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) means :: LATSUBGR:def 1
 for H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( ) ( ) LattStr ) ) holds it : ( ( Function-like V18(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) = the carrier of H : ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) ;
end;

theorem :: LATSUBGR:13
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for x being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) holds
( x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) iff x : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ;

theorem :: LATSUBGR:14
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds 1_ G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) in (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) ;

theorem :: LATSUBGR:15
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) ;

theorem :: LATSUBGR:16
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for g1, g2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st g1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) & g2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) holds
g1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) * g2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) in (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) ;

theorem :: LATSUBGR:17
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for g being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) in (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) holds
g : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) " : ( ( ) ( ) Element of the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) in (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) ;

theorem :: LATSUBGR:18
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds the carrier of (H1 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) /\ H2 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) = ((carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H1 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( ) ( ) set ) /\ ((carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H2 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

theorem :: LATSUBGR:19
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds (carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . (H1 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) /\ H2 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) = ((carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H1 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( ) ( ) set ) /\ ((carr G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , bool the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) . H2 : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

definition
let G be ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ;
let F be ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) ;
func meet F -> ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( ) ( ) LattStr ) ) means :: LATSUBGR:def 2
 the carrier of it : ( ( Function-like V18(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) = meet ((carr G : ( ( ) ( ) LattStr ) ) : ( ( Function-like V18( Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) , bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) ( Relation-like Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) -defined bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) -valued Function-like non empty V14( Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) V18( Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) , bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) ) Function of Subgroups G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) , bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) .: F : ( ( Function-like V18(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G : ( ( ) ( ) LattStr ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( ) Element of K19((bool the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) Element of K19(K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of K19( the carrier of G : ( ( ) ( ) LattStr ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ;
end;

theorem :: LATSUBGR:20
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for F being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) st (1). G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) in F : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) holds
meet F : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) = (1). G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

theorem :: LATSUBGR:21
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for h being ( ( ) ( ) Element of Subgroups G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) )
for F being ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) st F : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) = {h : ( ( ) ( ) Element of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) } : ( ( ) ( ) set ) holds
meet F : ( ( non empty ) ( non empty ) Subset of ( ( ) ( non empty ) set ) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) = h : ( ( ) ( ) Element of Subgroups b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUBGR:22
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for h1, h2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st h1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) & h2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds
h1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "\/" h2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) = H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) "\/" H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

theorem :: LATSUBGR:23
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for h1, h2 being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st h1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) & h2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds
h1 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) "/\" h2 : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) : ( ( ) ( ) Element of the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) = H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) /\ H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

theorem :: LATSUBGR:24
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for p being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) )
for H being ( ( ) ( non empty Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds
H : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is ( ( strict ) ( non empty strict Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

theorem :: LATSUBGR:25
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff the carrier of H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) c= the carrier of H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUBGR:26
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for H1, H2 being ( ( ) ( non empty Group-like ) Subgroup of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) )
for p, q being ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) st p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) & q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) = H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds
( p : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) [= q : ( ( ) ( ) Element of ( ( ) ( non empty ) set ) ) iff H1 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is ( ( ) ( non empty Group-like ) Subgroup of H2 : ( ( ) ( non empty Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ) ;

theorem :: LATSUBGR:27
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) holds lattice G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) is complete ;

definition
let G1, G2 be ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ;
let f be ( ( Function-like V18( the carrier of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ;
func FuncLatt f -> ( ( Function-like V18( the carrier of (lattice G1 : ( ( ) ( ) LattStr ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (lattice G1 : ( ( ) ( ) LattStr ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice G1 : ( ( ) ( ) LattStr ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice G1 : ( ( ) ( ) LattStr ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of (lattice G1 : ( ( ) ( ) LattStr ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like ) LattStr ) : ( ( ) ( non empty ) set ) ) means :: LATSUBGR:def 3
 for H being ( ( strict ) ( non empty strict Group-like ) Subgroup of G1 : ( ( ) ( ) LattStr ) )
for A being ( ( ) ( ) Subset of ) st A : ( ( ) ( ) Subset of ) = f : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) .: the carrier of H : ( ( strict ) ( non empty strict Group-like ) Subgroup of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( non empty ) set ) : ( ( ) ( ) Element of K19( the carrier of G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) holds
it : ( ( Function-like V18( the carrier of G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of f : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) ( Relation-like the carrier of G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -defined the carrier of f : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) -valued Function-like non empty V14( the carrier of G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) V18( the carrier of G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of f : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) ) Element of K19(K20( the carrier of G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) , the carrier of f : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) . H : ( ( strict ) ( non empty strict Group-like ) Subgroup of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) = gr A : ( ( ) ( ) Subset of ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of G2 : ( ( Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) ( Relation-like K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) -defined G1 : ( ( ) ( ) LattStr ) -valued Function-like V18(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) ) Element of K19(K20(K20(G1 : ( ( ) ( ) LattStr ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ,G1 : ( ( ) ( ) LattStr ) ) : ( ( ) ( ) set ) ) : ( ( ) ( non empty ) set ) ) ) ;
end;

theorem :: LATSUBGR:28
for G being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) holds FuncLatt (id the carrier of G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( Function-like V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) = id the carrier of (lattice G : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) : ( ( V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like one-to-one non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Element of K19(K20( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) : ( ( ) ( non empty ) set ) ) ;

theorem :: LATSUBGR:29
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is one-to-one holds
FuncLatt f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) is one-to-one ;

theorem :: LATSUBGR:30
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds (FuncLatt f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) : ( ( Function-like V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) . ((1). G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( ) ( ) set ) = (1). G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( strict ) ( non empty strict Group-like ) Subgroup of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ;

theorem :: LATSUBGR:31
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is one-to-one holds
FuncLatt f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Semilattice-Homomorphism of lattice G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) , lattice G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) ) ;

theorem :: LATSUBGR:32
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) holds FuncLatt f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) sup-Semilattice-Homomorphism of lattice G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) , lattice G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) ) ;

theorem :: LATSUBGR:33
for G1, G2 being ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group)
for f being ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) st f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) is one-to-one holds
FuncLatt f : ( ( Function-like V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) ( Relation-like the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -defined the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V18( the carrier of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) , the carrier of b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( ) ( non empty ) set ) ) V137(b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) ) Homomorphism of b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ,b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( Function-like V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Function of the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) is ( ( ) ( Relation-like the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -defined the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) -valued Function-like non empty V14( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) V18( the carrier of (lattice b1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) , the carrier of (lattice b2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) ) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) : ( ( ) ( non empty ) set ) ) ) Homomorphism of lattice G1 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) , lattice G2 : ( ( non empty Group-like V130() ) ( non empty Group-like V130() ) Group) : ( ( non empty strict Lattice-like ) ( non empty strict join-commutative join-associative meet-commutative meet-associative meet-absorbing join-absorbing Lattice-like lower-bounded upper-bounded V85() ) LattStr ) ) ;