let S be non empty RelStr ; :: thesis: for x being Element of S
for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X }
let x be Element of S; :: thesis: for X being Subset of S holds (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X }
let X be Subset of S; :: thesis: (x "/\") .: X = { (x "/\" y) where y is Element of S : y in X }
set Y = { (x "/\" y) where y is Element of S : y in X } ;
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { (x "/\" y) where y is Element of S : y in X } c= (x "/\") .: X
let y be object ; :: thesis: ( y in (x "/\") .: X implies y in { (x "/\" y) where y is Element of S : y in X } )
assume y in (x "/\") .: X ; :: thesis: y in { (x "/\" y) where y is Element of S : y in X }
then consider z being object such that
A1: z in the carrier of S and
A2: z in X and
A3: y = (x "/\") . z by FUNCT_2:64;
reconsider z = z as Element of S by A1;
y = x "/\" z by A3, Def18;
hence y in { (x "/\" y) where y is Element of S : y in X } by A2; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (x "/\" y) where y is Element of S : y in X } or y in (x "/\") .: X )
assume y in { (x "/\" y) where y is Element of S : y in X } ; :: thesis: y in (x "/\") .: X
then consider z being Element of S such that
A4: y = x "/\" z and
A5: z in X ;
y = (x "/\") . z by A4, Def18;
hence y in (x "/\") .: X by A5, FUNCT_2:35; :: thesis: verum