set X = [:D1,D2:];
[:D1,D2:] is filtered
proof
let x,
y be
Element of
[:S1,S2:];
:: according to WAYBEL_0:def 2 :: thesis: ( not x in [:D1,D2:] or not y in [:D1,D2:] or ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & b1 <= x & b1 <= y ) )
assume A1:
(
x in [:D1,D2:] &
y in [:D1,D2:] )
;
:: thesis: ex b1 being Element of the carrier of [:S1,S2:] st
( b1 in [:D1,D2:] & b1 <= x & b1 <= y )
then consider x1,
x2 being
set such that A2:
(
x1 in D1 &
x2 in D2 &
x = [x1,x2] )
by ZFMISC_1:def 2;
consider y1,
y2 being
set such that A3:
(
y1 in D1 &
y2 in D2 &
y = [y1,y2] )
by A1, ZFMISC_1:def 2;
reconsider x1 =
x1,
y1 =
y1 as
Element of
S1 by A2, A3;
reconsider x2 =
x2,
y2 =
y2 as
Element of
S2 by A2, A3;
consider xy1 being
Element of
S1 such that A4:
(
xy1 in D1 &
x1 >= xy1 &
y1 >= xy1 )
by A2, A3, WAYBEL_0:def 2;
consider xy2 being
Element of
S2 such that A5:
(
xy2 in D2 &
x2 >= xy2 &
y2 >= xy2 )
by A2, A3, WAYBEL_0:def 2;
reconsider S1' =
S1 as non
empty RelStr by A2;
reconsider S2' =
S2 as non
empty RelStr by A2;
reconsider xy1' =
xy1 as
Element of
S1' ;
reconsider xy2' =
xy2 as
Element of
S2' ;
[xy1',xy2'] is
Element of
[:S1',S2':]
;
then reconsider z =
[xy1,xy2] as
Element of
[:S1,S2:] ;
take
z
;
:: thesis: ( z in [:D1,D2:] & z <= x & z <= y )
thus
z in [:D1,D2:]
by A4, A5, ZFMISC_1:106;
:: thesis: ( z <= x & z <= y )
( not
S1 is
empty & not
S2 is
empty )
by A2;
hence
(
z <= x &
z <= y )
by A2, A3, A4, A5, Th11;
:: thesis: verum
end;
hence
[:D1,D2:] is filtered Subset of [:S1,S2:]
; :: thesis: verum