let L1, L2 be RelStr ; :: thesis: ( RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) implies for X1 being Subset of
for X2 being Subset of st X1 = X2 & X1 is filtered holds
X2 is filtered )
assume A1: RelStr(# the carrier of L1,the InternalRel of L1 #) = RelStr(# the carrier of L2,the InternalRel of L2 #) ; :: thesis: for X1 being Subset of
for X2 being Subset of st X1 = X2 & X1 is filtered holds
X2 is filtered
let X1 be Subset of ; :: thesis: for X2 being Subset of st X1 = X2 & X1 is filtered holds
X2 is filtered
let X2 be Subset of ; :: thesis: ( X1 = X2 & X1 is filtered implies X2 is filtered )
assume A2: X1 = X2 ; :: thesis: ( not X1 is filtered or X2 is filtered )
assume A3: for x, y being Element of st x in X1 & y in X1 holds
ex z being Element of st
( z in X1 & x >= z & y >= z ) ; :: according to WAYBEL_0:def 2 :: thesis: X2 is filtered
let x, y be Element of ; :: according to WAYBEL_0:def 2 :: thesis: ( x in X2 & y in X2 implies ex z being Element of st
( z in X2 & z <= x & z <= y ) )
reconsider x' = x, y' = y as Element of by A1;
assume that
A4: x in X2 and
A5: y in X2 ; :: thesis: ex z being Element of st
( z in X2 & z <= x & z <= y )
consider z' being Element of such that
A6: z' in X1 and
A7: x' >= z' and
A8: y' >= z' by A2, A3, A4, A5;
reconsider z = z' as Element of by A1;
take z ; :: thesis: ( z in X2 & z <= x & z <= y )
thus ( z in X2 & z <= x & z <= y ) by A1, A2, A6, A7, A8, YELLOW_0:1; :: thesis: verum