let alpha, beta be Ordinal; :: thesis: ( alpha c= beta implies ConwayDay alpha c= ConwayDay beta )
assume A1: alpha c= beta ; :: thesis: ConwayDay alpha c= ConwayDay beta
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in ConwayDay alpha or z in ConwayDay beta )
assume z in ConwayDay alpha ; :: thesis: z in ConwayDay beta
then consider w being strict left-right such that
A2: ( w = z & ( for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex gamma being Ordinal st
( gamma in alpha & e in ConwayDay gamma ) ) ) by Th1;
now :: thesis: for e being set st e in the LeftOptions of w \/ the RightOptions of w holds
ex gamma being Ordinal st
( gamma in beta & e in ConwayDay gamma )
let e be set ; :: thesis: ( e in the LeftOptions of w \/ the RightOptions of w implies ex gamma being Ordinal st
( gamma in beta & e in ConwayDay gamma ) )
assume e in the LeftOptions of w \/ the RightOptions of w ; :: thesis: ex gamma being Ordinal st
( gamma in beta & e in ConwayDay gamma )
then ex gamma being Ordinal st
( gamma in alpha & e in ConwayDay gamma ) by A2;
hence ex gamma being Ordinal st
( gamma in beta & e in ConwayDay gamma ) by A1; :: thesis: verum
end;
hence z in ConwayDay beta by Th1, A2; :: thesis: verum