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 a9 = a, b9 = b as Element of (SubstLatt (V,C)) ;
reconsider a1 = a, b1 = b as Element of SubstitutionSet (V,C) by SUBSTLAT:def 4;
A1: ( a9 % = a & b9 % = 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 a9 [= b9 by A1, LATTICE3:7;
then a9 = a9 "/\" b9 by LATTICES:4
.= the L_meet of (SubstLatt (V,C)) . (a9,b9) 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:4; :: 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:5;
then a9 = the L_meet of (SubstLatt (V,C)) . (a9,b9) by SUBSTLAT:def 4
.= a9 "/\" b9 by LATTICES:def 2 ;
then a9 [= b9 by LATTICES:4;
hence a <= b by A1, LATTICE3:7; :: thesis: verum