let V, C be set ; :: thesis: for a, b being Element of (SubstPoset V,C) holds
( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )
let a, b be Element of (SubstPoset V,C); :: thesis: ( a <= b iff for x being set st x in a holds
ex y being set st
( y in b & y c= x ) )
reconsider a' = a, b' = b as Element of (SubstLatt V,C) ;
reconsider a1 = a, b1 = b as Element of SubstitutionSet V,C by SUBSTLAT:def 4;
A1: ( a' % = a & b' % = b ) ;

hereby :: thesis: ( ( for x being set st x in a holds
ex y being set st
( y in b & y c= x ) ) implies a <= b )

assume a <= b ; :: thesis: for x being set st x in a holds
ex y being set st
( y in b & y c= x )
then a' [= b' by A1, LATTICE3:7;
then a' = a' "/\" b' by LATTICES:21
.= the L_meet of (SubstLatt V,C) . a',b' by LATTICES:def 2
.= mi (a1 ^ b1) by SUBSTLAT:def 4 ;
hence for x being set st x in a holds
ex y being set st
( y in b & y c= x ) by HEYTING2:8; :: thesis: verum

end;

assume for x being set st x in a holds
ex y being set st
( y in b & y c= x ) ; :: thesis: a <= b
then mi (a1 ^ b1) = a1 by HEYTING2:9;
then a' = the L_meet of (SubstLatt V,C) . a',b' by SUBSTLAT:def 4
.= a' "/\" b' by LATTICES:def 2 ;
then a' [= b' by LATTICES:21;
hence a <= b by A1, LATTICE3:7; :: thesis: verum